homotopy theory, (∞,1)-category theory, homotopy type theory
flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…
models: topological, simplicial, localic, …
see also algebraic topology
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
A vector space is finite-dimensional if it admits a finite basis: if there exists a natural number such that the vector space admits a linear isomorphism to the direct sum of copies of the underlying vector space of the ground field.
The category FinDimVect of finite-dimensional vector spaces is of course the full subcategory of Vect whose objects are finite-dimensional.
A vector space is finite-dimensional precisely if the hom-functor preserves filtered colimits.
Notice that every vector space is the filtered colimit of the diagram of finite-dimensional subspaces and inclusions between them. Applying this to , the condition that preserves filtered colimits implies that the canonical comparison map from the following filtered colimit over the finite-dimensional subspaces is an isomorphism:
Therfore some element in the colimit represented by gets mapped to the identity , i.e., for some inclusion . This implies is an isomorphism, so that is finite-dimensional.
In the converse direction, observe that has a right adjoint (and hence preserves all colimits) if is finite-dimensional.
To see this, first notice that the dual vector space of functionals to the ground field is a dual object to in the sense of monoidal category theory, so that there is a counit (evaluation map)
The unit is uniquely determined from this counit and can be described using any linear basis of and dual basis as the map
We thus have an adjunction
whose mate is, by the internal hom-adjunction of this form:
exhibiting the desired right adjoint to .
Finite-dimensional vector spaces are exactly the compact objects of Vect in the sense of locally presentable categories, but also the compact = dualizable objects in the sense of monoidal category theory. In particular the category FinDimVect is a compact closed category.
Discussion of finite-dimensional vector spaces as categorical semantics for linear logic/linear type theory:
Benoît Valiron, Steve Zdancewic, Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi, in: Proc. of ICTAC’14, Lecture Notes in Computer Science 8687, Springer (2014) 442-459 [arXiv:1406.1310, doi:10.1007/978-3-319-10882-7_26, slides:pdf, pdf]
(focus on finite ground fields)
Daniel Murfet, Logic and linear algebra: an introduction [arXiv:1407.2650]
Last revised on September 12, 2023 at 06:21:10. See the history of this page for a list of all contributions to it.